a, b:. a = b  a=b 

latex

Definitions	, t  T, x:A. B(x), Prop, AB, P  Q, False, A, True, T, P  Q, P & Q, P  Q, i=j, b, x. t(x)
Lemmas	all functionality wrt iff, iff functionality wrt iff, assert of eq int, iff wf, assert wf, eq int wf, le wf, nat wf